choicef(${\it xm}$; $T$; $x$.$P$($x$)) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Case ${\it xm}$(\{$y$:$T$$\mid$ $P$($y$) \}) of inl($z$) $\Rightarrow$ $z$ ; inr($w$) $\Rightarrow$ "???"